$\forall$${\it es}$:ES\{i\}, $A$:Type\{i\}, $X$:AbsInterface($A$). es{-}interface{-}local\{i:l\}(${\it es}$; $A$; $X$) $\in$ $\mathbb{P}$\{i'\}